KILLED



    


Runtime Complexity (innermost) proof of /tmp/tmpgIJB8v/splitandsort.raml.xml









The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, INF).

0 CpxRelTRS


↳1 DecreasingLoopProof (⇔, 1873 ms)


↳2 BOUNDS(n^1, INF)


↳3 RenamingProof (⇔, 3 ms)


↳4 CpxRelTRS


    ↳5 TypeInferenceProof (BOTH BOUNDS(ID, ID), 0 ms)


    ↳6 typed CpxTrs


    ↳7 OrderProof (LOWER BOUND(ID), 0 ms)


    ↳8 typed CpxTrs









(0) Obligation:
Runtime Complexity Relative TRS:
The TRS R consists of the following rules:

#equal(@x, @y) → #eq(@x, @y)

#greater(@x, @y) → #ckgt(#compare(@x, @y))

append(@l, @ys) → append#1(@l, @ys)

append#1(::(@x, @xs), @ys) → ::(@x, append(@xs, @ys))

append#1(nil, @ys) → @ys

insert(@x, @l) → insert#1(@x, @l, @x)

insert#1(tuple#2(@valX, @keyX), @l, @x) → insert#2(@l, @keyX, @valX, @x)

insert#2(::(@l1, @ls), @keyX, @valX, @x) → insert#3(@l1, @keyX, @ls, @valX, @x)

insert#2(nil, @keyX, @valX, @x) → ::(tuple#2(::(@valX, nil), @keyX), nil)

insert#3(tuple#2(@vals1, @key1), @keyX, @ls, @valX, @x) → insert#4(#equal(@key1, @keyX), @key1, @ls, @valX, @vals1, @x)

insert#4(#false, @key1, @ls, @valX, @vals1, @x) → ::(tuple#2(@vals1, @key1), insert(@x, @ls))

insert#4(#true, @key1, @ls, @valX, @vals1, @x) → ::(tuple#2(::(@valX, @vals1), @key1), @ls)

quicksort(@l) → quicksort#1(@l)

quicksort#1(::(@z, @zs)) → quicksort#2(splitqs(@z, @zs), @z)

quicksort#1(nil) → nil

quicksort#2(tuple#2(@xs, @ys), @z) → append(quicksort(@xs), ::(@z, quicksort(@ys)))

sortAll(@l) → sortAll#1(@l)

sortAll#1(::(@x, @xs)) → sortAll#2(@x, @xs)

sortAll#1(nil) → nil

sortAll#2(tuple#2(@vals, @key), @xs) → ::(tuple#2(quicksort(@vals), @key), sortAll(@xs))

split(@l) → split#1(@l)

split#1(::(@x, @xs)) → insert(@x, split(@xs))

split#1(nil) → nil

splitAndSort(@l) → sortAll(split(@l))

splitqs(@pivot, @l) → splitqs#1(@l, @pivot)

splitqs#1(::(@x, @xs), @pivot) → splitqs#2(splitqs(@pivot, @xs), @pivot, @x)

splitqs#1(nil, @pivot) → tuple#2(nil, nil)

splitqs#2(tuple#2(@ls, @rs), @pivot, @x) → splitqs#3(#greater(@x, @pivot), @ls, @rs, @x)

splitqs#3(#false, @ls, @rs, @x) → tuple#2(::(@x, @ls), @rs)

splitqs#3(#true, @ls, @rs, @x) → tuple#2(@ls, ::(@x, @rs))

The (relative) TRS S consists of the following rules:

#and(#false, #false) → #false

#and(#false, #true) → #false

#and(#true, #false) → #false

#and(#true, #true) → #true

#ckgt(#EQ) → #false

#ckgt(#GT) → #true

#ckgt(#LT) → #false

#compare(#0, #0) → #EQ

#compare(#0, #neg(@y)) → #GT

#compare(#0, #pos(@y)) → #LT

#compare(#0, #s(@y)) → #LT

#compare(#neg(@x), #0) → #LT

#compare(#neg(@x), #neg(@y)) → #compare(@y, @x)

#compare(#neg(@x), #pos(@y)) → #LT

#compare(#pos(@x), #0) → #GT

#compare(#pos(@x), #neg(@y)) → #GT

#compare(#pos(@x), #pos(@y)) → #compare(@x, @y)

#compare(#s(@x), #0) → #GT

#compare(#s(@x), #s(@y)) → #compare(@x, @y)

#eq(#0, #0) → #true

#eq(#0, #neg(@y)) → #false

#eq(#0, #pos(@y)) → #false

#eq(#0, #s(@y)) → #false

#eq(#neg(@x), #0) → #false

#eq(#neg(@x), #neg(@y)) → #eq(@x, @y)

#eq(#neg(@x), #pos(@y)) → #false

#eq(#pos(@x), #0) → #false

#eq(#pos(@x), #neg(@y)) → #false

#eq(#pos(@x), #pos(@y)) → #eq(@x, @y)

#eq(#s(@x), #0) → #false

#eq(#s(@x), #s(@y)) → #eq(@x, @y)

#eq(::(@x_1, @x_2), ::(@y_1, @y_2)) → #and(#eq(@x_1, @y_1), #eq(@x_2, @y_2))

#eq(::(@x_1, @x_2), nil) → #false

#eq(::(@x_1, @x_2), tuple#2(@y_1, @y_2)) → #false

#eq(nil, ::(@y_1, @y_2)) → #false

#eq(nil, nil) → #true

#eq(nil, tuple#2(@y_1, @y_2)) → #false

#eq(tuple#2(@x_1, @x_2), ::(@y_1, @y_2)) → #false

#eq(tuple#2(@x_1, @x_2), nil) → #false

#eq(tuple#2(@x_1, @x_2), tuple#2(@y_1, @y_2)) → #and(#eq(@x_1, @y_1), #eq(@x_2, @y_2))

Rewrite Strategy: INNERMOST




(1) DecreasingLoopProof (EQUIVALENT transformation)
The following loop(s) give(s) rise to the lower bound Ω(n1):
The rewrite sequence
append(::(@x15111_5, @xs15112_5), @ys) →+ ::(@x15111_5, append(@xs15112_5, @ys))
gives rise to a decreasing loop by considering the right hand sides subterm at position [1].
The pumping substitution is [@xs15112_5 / ::(@x15111_5, @xs15112_5)].
The result substitution is [ ].





(2) BOUNDS(n^1, INF)




(3) RenamingProof (EQUIVALENT transformation)
Renamed function symbols to avoid clashes with predefined symbol.




(4) Obligation:
Runtime Complexity Relative TRS:
The TRS R consists of the following rules:

#equal(@x, @y) → #eq(@x, @y)

#greater(@x, @y) → #ckgt(#compare(@x, @y))

append(@l, @ys) → append#1(@l, @ys)

append#1(::(@x, @xs), @ys) → ::(@x, append(@xs, @ys))

append#1(nil, @ys) → @ys

insert(@x, @l) → insert#1(@x, @l, @x)

insert#1(tuple#2(@valX, @keyX), @l, @x) → insert#2(@l, @keyX, @valX, @x)

insert#2(::(@l1, @ls), @keyX, @valX, @x) → insert#3(@l1, @keyX, @ls, @valX, @x)

insert#2(nil, @keyX, @valX, @x) → ::(tuple#2(::(@valX, nil), @keyX), nil)

insert#3(tuple#2(@vals1, @key1), @keyX, @ls, @valX, @x) → insert#4(#equal(@key1, @keyX), @key1, @ls, @valX, @vals1, @x)

insert#4(#false, @key1, @ls, @valX, @vals1, @x) → ::(tuple#2(@vals1, @key1), insert(@x, @ls))

insert#4(#true, @key1, @ls, @valX, @vals1, @x) → ::(tuple#2(::(@valX, @vals1), @key1), @ls)

quicksort(@l) → quicksort#1(@l)

quicksort#1(::(@z, @zs)) → quicksort#2(splitqs(@z, @zs), @z)

quicksort#1(nil) → nil

quicksort#2(tuple#2(@xs, @ys), @z) → append(quicksort(@xs), ::(@z, quicksort(@ys)))

sortAll(@l) → sortAll#1(@l)

sortAll#1(::(@x, @xs)) → sortAll#2(@x, @xs)

sortAll#1(nil) → nil

sortAll#2(tuple#2(@vals, @key), @xs) → ::(tuple#2(quicksort(@vals), @key), sortAll(@xs))

split(@l) → split#1(@l)

split#1(::(@x, @xs)) → insert(@x, split(@xs))

split#1(nil) → nil

splitAndSort(@l) → sortAll(split(@l))

splitqs(@pivot, @l) → splitqs#1(@l, @pivot)

splitqs#1(::(@x, @xs), @pivot) → splitqs#2(splitqs(@pivot, @xs), @pivot, @x)

splitqs#1(nil, @pivot) → tuple#2(nil, nil)

splitqs#2(tuple#2(@ls, @rs), @pivot, @x) → splitqs#3(#greater(@x, @pivot), @ls, @rs, @x)

splitqs#3(#false, @ls, @rs, @x) → tuple#2(::(@x, @ls), @rs)

splitqs#3(#true, @ls, @rs, @x) → tuple#2(@ls, ::(@x, @rs))

The (relative) TRS S consists of the following rules:

#and(#false, #false) → #false

#and(#false, #true) → #false

#and(#true, #false) → #false

#and(#true, #true) → #true

#ckgt(#EQ) → #false

#ckgt(#GT) → #true

#ckgt(#LT) → #false

#compare(#0, #0) → #EQ

#compare(#0, #neg(@y)) → #GT

#compare(#0, #pos(@y)) → #LT

#compare(#0, #s(@y)) → #LT

#compare(#neg(@x), #0) → #LT

#compare(#neg(@x), #neg(@y)) → #compare(@y, @x)

#compare(#neg(@x), #pos(@y)) → #LT

#compare(#pos(@x), #0) → #GT

#compare(#pos(@x), #neg(@y)) → #GT

#compare(#pos(@x), #pos(@y)) → #compare(@x, @y)

#compare(#s(@x), #0) → #GT

#compare(#s(@x), #s(@y)) → #compare(@x, @y)

#eq(#0, #0) → #true

#eq(#0, #neg(@y)) → #false

#eq(#0, #pos(@y)) → #false

#eq(#0, #s(@y)) → #false

#eq(#neg(@x), #0) → #false

#eq(#neg(@x), #neg(@y)) → #eq(@x, @y)

#eq(#neg(@x), #pos(@y)) → #false

#eq(#pos(@x), #0) → #false

#eq(#pos(@x), #neg(@y)) → #false

#eq(#pos(@x), #pos(@y)) → #eq(@x, @y)

#eq(#s(@x), #0) → #false

#eq(#s(@x), #s(@y)) → #eq(@x, @y)

#eq(::(@x_1, @x_2), ::(@y_1, @y_2)) → #and(#eq(@x_1, @y_1), #eq(@x_2, @y_2))

#eq(::(@x_1, @x_2), nil) → #false

#eq(::(@x_1, @x_2), tuple#2(@y_1, @y_2)) → #false

#eq(nil, ::(@y_1, @y_2)) → #false

#eq(nil, nil) → #true

#eq(nil, tuple#2(@y_1, @y_2)) → #false

#eq(tuple#2(@x_1, @x_2), ::(@y_1, @y_2)) → #false

#eq(tuple#2(@x_1, @x_2), nil) → #false

#eq(tuple#2(@x_1, @x_2), tuple#2(@y_1, @y_2)) → #and(#eq(@x_1, @y_1), #eq(@x_2, @y_2))

Rewrite Strategy: INNERMOST




(5) TypeInferenceProof (BOTH BOUNDS(ID, ID) transformation)
Infered types.




(6) Obligation:
Innermost TRS:
Rules:
#equal(@x, @y) → #eq(@x, @y)
#greater(@x, @y) → #ckgt(#compare(@x, @y))
append(@l, @ys) → append#1(@l, @ys)
append#1(::(@x, @xs), @ys) → ::(@x, append(@xs, @ys))
append#1(nil, @ys) → @ys
insert(@x, @l) → insert#1(@x, @l, @x)
insert#1(tuple#2(@valX, @keyX), @l, @x) → insert#2(@l, @keyX, @valX, @x)
insert#2(::(@l1, @ls), @keyX, @valX, @x) → insert#3(@l1, @keyX, @ls, @valX, @x)
insert#2(nil, @keyX, @valX, @x) → ::(tuple#2(::(@valX, nil), @keyX), nil)
insert#3(tuple#2(@vals1, @key1), @keyX, @ls, @valX, @x) → insert#4(#equal(@key1, @keyX), @key1, @ls, @valX, @vals1, @x)
insert#4(#false, @key1, @ls, @valX, @vals1, @x) → ::(tuple#2(@vals1, @key1), insert(@x, @ls))
insert#4(#true, @key1, @ls, @valX, @vals1, @x) → ::(tuple#2(::(@valX, @vals1), @key1), @ls)
quicksort(@l) → quicksort#1(@l)
quicksort#1(::(@z, @zs)) → quicksort#2(splitqs(@z, @zs), @z)
quicksort#1(nil) → nil
quicksort#2(tuple#2(@xs, @ys), @z) → append(quicksort(@xs), ::(@z, quicksort(@ys)))
sortAll(@l) → sortAll#1(@l)
sortAll#1(::(@x, @xs)) → sortAll#2(@x, @xs)
sortAll#1(nil) → nil
sortAll#2(tuple#2(@vals, @key), @xs) → ::(tuple#2(quicksort(@vals), @key), sortAll(@xs))
split(@l) → split#1(@l)
split#1(::(@x, @xs)) → insert(@x, split(@xs))
split#1(nil) → nil
splitAndSort(@l) → sortAll(split(@l))
splitqs(@pivot, @l) → splitqs#1(@l, @pivot)
splitqs#1(::(@x, @xs), @pivot) → splitqs#2(splitqs(@pivot, @xs), @pivot, @x)
splitqs#1(nil, @pivot) → tuple#2(nil, nil)
splitqs#2(tuple#2(@ls, @rs), @pivot, @x) → splitqs#3(#greater(@x, @pivot), @ls, @rs, @x)
splitqs#3(#false, @ls, @rs, @x) → tuple#2(::(@x, @ls), @rs)
splitqs#3(#true, @ls, @rs, @x) → tuple#2(@ls, ::(@x, @rs))
#and(#false, #false) → #false
#and(#false, #true) → #false
#and(#true, #false) → #false
#and(#true, #true) → #true
#ckgt(#EQ) → #false
#ckgt(#GT) → #true
#ckgt(#LT) → #false
#compare(#0, #0) → #EQ
#compare(#0, #neg(@y)) → #GT
#compare(#0, #pos(@y)) → #LT
#compare(#0, #s(@y)) → #LT
#compare(#neg(@x), #0) → #LT
#compare(#neg(@x), #neg(@y)) → #compare(@y, @x)
#compare(#neg(@x), #pos(@y)) → #LT
#compare(#pos(@x), #0) → #GT
#compare(#pos(@x), #neg(@y)) → #GT
#compare(#pos(@x), #pos(@y)) → #compare(@x, @y)
#compare(#s(@x), #0) → #GT
#compare(#s(@x), #s(@y)) → #compare(@x, @y)
#eq(#0, #0) → #true
#eq(#0, #neg(@y)) → #false
#eq(#0, #pos(@y)) → #false
#eq(#0, #s(@y)) → #false
#eq(#neg(@x), #0) → #false
#eq(#neg(@x), #neg(@y)) → #eq(@x, @y)
#eq(#neg(@x), #pos(@y)) → #false
#eq(#pos(@x), #0) → #false
#eq(#pos(@x), #neg(@y)) → #false
#eq(#pos(@x), #pos(@y)) → #eq(@x, @y)
#eq(#s(@x), #0) → #false
#eq(#s(@x), #s(@y)) → #eq(@x, @y)
#eq(::(@x_1, @x_2), ::(@y_1, @y_2)) → #and(#eq(@x_1, @y_1), #eq(@x_2, @y_2))
#eq(::(@x_1, @x_2), nil) → #false
#eq(::(@x_1, @x_2), tuple#2(@y_1, @y_2)) → #false
#eq(nil, ::(@y_1, @y_2)) → #false
#eq(nil, nil) → #true
#eq(nil, tuple#2(@y_1, @y_2)) → #false
#eq(tuple#2(@x_1, @x_2), ::(@y_1, @y_2)) → #false
#eq(tuple#2(@x_1, @x_2), nil) → #false
#eq(tuple#2(@x_1, @x_2), tuple#2(@y_1, @y_2)) → #and(#eq(@x_1, @y_1), #eq(@x_2, @y_2))

Types:
#equal :: :::nil:tuple#2:#0:#neg:#pos:#s → :::nil:tuple#2:#0:#neg:#pos:#s → #false:#true
#eq :: :::nil:tuple#2:#0:#neg:#pos:#s → :::nil:tuple#2:#0:#neg:#pos:#s → #false:#true
#greater :: :::nil:tuple#2:#0:#neg:#pos:#s → :::nil:tuple#2:#0:#neg:#pos:#s → #false:#true
#ckgt :: #EQ:#GT:#LT → #false:#true
#compare :: :::nil:tuple#2:#0:#neg:#pos:#s → :::nil:tuple#2:#0:#neg:#pos:#s → #EQ:#GT:#LT
append :: :::nil:tuple#2:#0:#neg:#pos:#s → :::nil:tuple#2:#0:#neg:#pos:#s → :::nil:tuple#2:#0:#neg:#pos:#s
append#1 :: :::nil:tuple#2:#0:#neg:#pos:#s → :::nil:tuple#2:#0:#neg:#pos:#s → :::nil:tuple#2:#0:#neg:#pos:#s
:: :: :::nil:tuple#2:#0:#neg:#pos:#s → :::nil:tuple#2:#0:#neg:#pos:#s → :::nil:tuple#2:#0:#neg:#pos:#s
nil :: :::nil:tuple#2:#0:#neg:#pos:#s
insert :: :::nil:tuple#2:#0:#neg:#pos:#s → :::nil:tuple#2:#0:#neg:#pos:#s → :::nil:tuple#2:#0:#neg:#pos:#s
insert#1 :: :::nil:tuple#2:#0:#neg:#pos:#s → :::nil:tuple#2:#0:#neg:#pos:#s → :::nil:tuple#2:#0:#neg:#pos:#s → :::nil:tuple#2:#0:#neg:#pos:#s
tuple#2 :: :::nil:tuple#2:#0:#neg:#pos:#s → :::nil:tuple#2:#0:#neg:#pos:#s → :::nil:tuple#2:#0:#neg:#pos:#s
insert#2 :: :::nil:tuple#2:#0:#neg:#pos:#s → :::nil:tuple#2:#0:#neg:#pos:#s → :::nil:tuple#2:#0:#neg:#pos:#s → :::nil:tuple#2:#0:#neg:#pos:#s → :::nil:tuple#2:#0:#neg:#pos:#s
insert#3 :: :::nil:tuple#2:#0:#neg:#pos:#s → :::nil:tuple#2:#0:#neg:#pos:#s → :::nil:tuple#2:#0:#neg:#pos:#s → :::nil:tuple#2:#0:#neg:#pos:#s → :::nil:tuple#2:#0:#neg:#pos:#s → :::nil:tuple#2:#0:#neg:#pos:#s
insert#4 :: #false:#true → :::nil:tuple#2:#0:#neg:#pos:#s → :::nil:tuple#2:#0:#neg:#pos:#s → :::nil:tuple#2:#0:#neg:#pos:#s → :::nil:tuple#2:#0:#neg:#pos:#s → :::nil:tuple#2:#0:#neg:#pos:#s → :::nil:tuple#2:#0:#neg:#pos:#s
#false :: #false:#true
#true :: #false:#true
quicksort :: :::nil:tuple#2:#0:#neg:#pos:#s → :::nil:tuple#2:#0:#neg:#pos:#s
quicksort#1 :: :::nil:tuple#2:#0:#neg:#pos:#s → :::nil:tuple#2:#0:#neg:#pos:#s
quicksort#2 :: :::nil:tuple#2:#0:#neg:#pos:#s → :::nil:tuple#2:#0:#neg:#pos:#s → :::nil:tuple#2:#0:#neg:#pos:#s
splitqs :: :::nil:tuple#2:#0:#neg:#pos:#s → :::nil:tuple#2:#0:#neg:#pos:#s → :::nil:tuple#2:#0:#neg:#pos:#s
sortAll :: :::nil:tuple#2:#0:#neg:#pos:#s → :::nil:tuple#2:#0:#neg:#pos:#s
sortAll#1 :: :::nil:tuple#2:#0:#neg:#pos:#s → :::nil:tuple#2:#0:#neg:#pos:#s
sortAll#2 :: :::nil:tuple#2:#0:#neg:#pos:#s → :::nil:tuple#2:#0:#neg:#pos:#s → :::nil:tuple#2:#0:#neg:#pos:#s
split :: :::nil:tuple#2:#0:#neg:#pos:#s → :::nil:tuple#2:#0:#neg:#pos:#s
split#1 :: :::nil:tuple#2:#0:#neg:#pos:#s → :::nil:tuple#2:#0:#neg:#pos:#s
splitAndSort :: :::nil:tuple#2:#0:#neg:#pos:#s → :::nil:tuple#2:#0:#neg:#pos:#s
splitqs#1 :: :::nil:tuple#2:#0:#neg:#pos:#s → :::nil:tuple#2:#0:#neg:#pos:#s → :::nil:tuple#2:#0:#neg:#pos:#s
splitqs#2 :: :::nil:tuple#2:#0:#neg:#pos:#s → :::nil:tuple#2:#0:#neg:#pos:#s → :::nil:tuple#2:#0:#neg:#pos:#s → :::nil:tuple#2:#0:#neg:#pos:#s
splitqs#3 :: #false:#true → :::nil:tuple#2:#0:#neg:#pos:#s → :::nil:tuple#2:#0:#neg:#pos:#s → :::nil:tuple#2:#0:#neg:#pos:#s → :::nil:tuple#2:#0:#neg:#pos:#s
#and :: #false:#true → #false:#true → #false:#true
#EQ :: #EQ:#GT:#LT
#GT :: #EQ:#GT:#LT
#LT :: #EQ:#GT:#LT
#0 :: :::nil:tuple#2:#0:#neg:#pos:#s
#neg :: :::nil:tuple#2:#0:#neg:#pos:#s → :::nil:tuple#2:#0:#neg:#pos:#s
#pos :: :::nil:tuple#2:#0:#neg:#pos:#s → :::nil:tuple#2:#0:#neg:#pos:#s
#s :: :::nil:tuple#2:#0:#neg:#pos:#s → :::nil:tuple#2:#0:#neg:#pos:#s
hole_#false:#true1_5 :: #false:#true
hole_:::nil:tuple#2:#0:#neg:#pos:#s2_5 :: :::nil:tuple#2:#0:#neg:#pos:#s
hole_#EQ:#GT:#LT3_5 :: #EQ:#GT:#LT
gen_:::nil:tuple#2:#0:#neg:#pos:#s4_5 :: Nat → :::nil:tuple#2:#0:#neg:#pos:#s




(7) OrderProof (LOWER BOUND(ID) transformation)
Heuristically decided to analyse the following defined symbols:
#eq, #compare, append, append#1, insert, quicksort, quicksort#1, splitqs, sortAll, sortAll#1, split, split#1, splitqs#1
They will be analysed ascendingly in the following order:
append = append#1
append < quicksort#1
insert < split#1
quicksort = quicksort#1
quicksort < sortAll#1
splitqs < quicksort#1
splitqs = splitqs#1
sortAll = sortAll#1
split = split#1




(8) Obligation:
Innermost TRS:
Rules:
#equal(@x, @y) → #eq(@x, @y)
#greater(@x, @y) → #ckgt(#compare(@x, @y))
append(@l, @ys) → append#1(@l, @ys)
append#1(::(@x, @xs), @ys) → ::(@x, append(@xs, @ys))
append#1(nil, @ys) → @ys
insert(@x, @l) → insert#1(@x, @l, @x)
insert#1(tuple#2(@valX, @keyX), @l, @x) → insert#2(@l, @keyX, @valX, @x)
insert#2(::(@l1, @ls), @keyX, @valX, @x) → insert#3(@l1, @keyX, @ls, @valX, @x)
insert#2(nil, @keyX, @valX, @x) → ::(tuple#2(::(@valX, nil), @keyX), nil)
insert#3(tuple#2(@vals1, @key1), @keyX, @ls, @valX, @x) → insert#4(#equal(@key1, @keyX), @key1, @ls, @valX, @vals1, @x)
insert#4(#false, @key1, @ls, @valX, @vals1, @x) → ::(tuple#2(@vals1, @key1), insert(@x, @ls))
insert#4(#true, @key1, @ls, @valX, @vals1, @x) → ::(tuple#2(::(@valX, @vals1), @key1), @ls)
quicksort(@l) → quicksort#1(@l)
quicksort#1(::(@z, @zs)) → quicksort#2(splitqs(@z, @zs), @z)
quicksort#1(nil) → nil
quicksort#2(tuple#2(@xs, @ys), @z) → append(quicksort(@xs), ::(@z, quicksort(@ys)))
sortAll(@l) → sortAll#1(@l)
sortAll#1(::(@x, @xs)) → sortAll#2(@x, @xs)
sortAll#1(nil) → nil
sortAll#2(tuple#2(@vals, @key), @xs) → ::(tuple#2(quicksort(@vals), @key), sortAll(@xs))
split(@l) → split#1(@l)
split#1(::(@x, @xs)) → insert(@x, split(@xs))
split#1(nil) → nil
splitAndSort(@l) → sortAll(split(@l))
splitqs(@pivot, @l) → splitqs#1(@l, @pivot)
splitqs#1(::(@x, @xs), @pivot) → splitqs#2(splitqs(@pivot, @xs), @pivot, @x)
splitqs#1(nil, @pivot) → tuple#2(nil, nil)
splitqs#2(tuple#2(@ls, @rs), @pivot, @x) → splitqs#3(#greater(@x, @pivot), @ls, @rs, @x)
splitqs#3(#false, @ls, @rs, @x) → tuple#2(::(@x, @ls), @rs)
splitqs#3(#true, @ls, @rs, @x) → tuple#2(@ls, ::(@x, @rs))
#and(#false, #false) → #false
#and(#false, #true) → #false
#and(#true, #false) → #false
#and(#true, #true) → #true
#ckgt(#EQ) → #false
#ckgt(#GT) → #true
#ckgt(#LT) → #false
#compare(#0, #0) → #EQ
#compare(#0, #neg(@y)) → #GT
#compare(#0, #pos(@y)) → #LT
#compare(#0, #s(@y)) → #LT
#compare(#neg(@x), #0) → #LT
#compare(#neg(@x), #neg(@y)) → #compare(@y, @x)
#compare(#neg(@x), #pos(@y)) → #LT
#compare(#pos(@x), #0) → #GT
#compare(#pos(@x), #neg(@y)) → #GT
#compare(#pos(@x), #pos(@y)) → #compare(@x, @y)
#compare(#s(@x), #0) → #GT
#compare(#s(@x), #s(@y)) → #compare(@x, @y)
#eq(#0, #0) → #true
#eq(#0, #neg(@y)) → #false
#eq(#0, #pos(@y)) → #false
#eq(#0, #s(@y)) → #false
#eq(#neg(@x), #0) → #false
#eq(#neg(@x), #neg(@y)) → #eq(@x, @y)
#eq(#neg(@x), #pos(@y)) → #false
#eq(#pos(@x), #0) → #false
#eq(#pos(@x), #neg(@y)) → #false
#eq(#pos(@x), #pos(@y)) → #eq(@x, @y)
#eq(#s(@x), #0) → #false
#eq(#s(@x), #s(@y)) → #eq(@x, @y)
#eq(::(@x_1, @x_2), ::(@y_1, @y_2)) → #and(#eq(@x_1, @y_1), #eq(@x_2, @y_2))
#eq(::(@x_1, @x_2), nil) → #false
#eq(::(@x_1, @x_2), tuple#2(@y_1, @y_2)) → #false
#eq(nil, ::(@y_1, @y_2)) → #false
#eq(nil, nil) → #true
#eq(nil, tuple#2(@y_1, @y_2)) → #false
#eq(tuple#2(@x_1, @x_2), ::(@y_1, @y_2)) → #false
#eq(tuple#2(@x_1, @x_2), nil) → #false
#eq(tuple#2(@x_1, @x_2), tuple#2(@y_1, @y_2)) → #and(#eq(@x_1, @y_1), #eq(@x_2, @y_2))

Types:
#equal :: :::nil:tuple#2:#0:#neg:#pos:#s → :::nil:tuple#2:#0:#neg:#pos:#s → #false:#true
#eq :: :::nil:tuple#2:#0:#neg:#pos:#s → :::nil:tuple#2:#0:#neg:#pos:#s → #false:#true
#greater :: :::nil:tuple#2:#0:#neg:#pos:#s → :::nil:tuple#2:#0:#neg:#pos:#s → #false:#true
#ckgt :: #EQ:#GT:#LT → #false:#true
#compare :: :::nil:tuple#2:#0:#neg:#pos:#s → :::nil:tuple#2:#0:#neg:#pos:#s → #EQ:#GT:#LT
append :: :::nil:tuple#2:#0:#neg:#pos:#s → :::nil:tuple#2:#0:#neg:#pos:#s → :::nil:tuple#2:#0:#neg:#pos:#s
append#1 :: :::nil:tuple#2:#0:#neg:#pos:#s → :::nil:tuple#2:#0:#neg:#pos:#s → :::nil:tuple#2:#0:#neg:#pos:#s
:: :: :::nil:tuple#2:#0:#neg:#pos:#s → :::nil:tuple#2:#0:#neg:#pos:#s → :::nil:tuple#2:#0:#neg:#pos:#s
nil :: :::nil:tuple#2:#0:#neg:#pos:#s
insert :: :::nil:tuple#2:#0:#neg:#pos:#s → :::nil:tuple#2:#0:#neg:#pos:#s → :::nil:tuple#2:#0:#neg:#pos:#s
insert#1 :: :::nil:tuple#2:#0:#neg:#pos:#s → :::nil:tuple#2:#0:#neg:#pos:#s → :::nil:tuple#2:#0:#neg:#pos:#s → :::nil:tuple#2:#0:#neg:#pos:#s
tuple#2 :: :::nil:tuple#2:#0:#neg:#pos:#s → :::nil:tuple#2:#0:#neg:#pos:#s → :::nil:tuple#2:#0:#neg:#pos:#s
insert#2 :: :::nil:tuple#2:#0:#neg:#pos:#s → :::nil:tuple#2:#0:#neg:#pos:#s → :::nil:tuple#2:#0:#neg:#pos:#s → :::nil:tuple#2:#0:#neg:#pos:#s → :::nil:tuple#2:#0:#neg:#pos:#s
insert#3 :: :::nil:tuple#2:#0:#neg:#pos:#s → :::nil:tuple#2:#0:#neg:#pos:#s → :::nil:tuple#2:#0:#neg:#pos:#s → :::nil:tuple#2:#0:#neg:#pos:#s → :::nil:tuple#2:#0:#neg:#pos:#s → :::nil:tuple#2:#0:#neg:#pos:#s
insert#4 :: #false:#true → :::nil:tuple#2:#0:#neg:#pos:#s → :::nil:tuple#2:#0:#neg:#pos:#s → :::nil:tuple#2:#0:#neg:#pos:#s → :::nil:tuple#2:#0:#neg:#pos:#s → :::nil:tuple#2:#0:#neg:#pos:#s → :::nil:tuple#2:#0:#neg:#pos:#s
#false :: #false:#true
#true :: #false:#true
quicksort :: :::nil:tuple#2:#0:#neg:#pos:#s → :::nil:tuple#2:#0:#neg:#pos:#s
quicksort#1 :: :::nil:tuple#2:#0:#neg:#pos:#s → :::nil:tuple#2:#0:#neg:#pos:#s
quicksort#2 :: :::nil:tuple#2:#0:#neg:#pos:#s → :::nil:tuple#2:#0:#neg:#pos:#s → :::nil:tuple#2:#0:#neg:#pos:#s
splitqs :: :::nil:tuple#2:#0:#neg:#pos:#s → :::nil:tuple#2:#0:#neg:#pos:#s → :::nil:tuple#2:#0:#neg:#pos:#s
sortAll :: :::nil:tuple#2:#0:#neg:#pos:#s → :::nil:tuple#2:#0:#neg:#pos:#s
sortAll#1 :: :::nil:tuple#2:#0:#neg:#pos:#s → :::nil:tuple#2:#0:#neg:#pos:#s
sortAll#2 :: :::nil:tuple#2:#0:#neg:#pos:#s → :::nil:tuple#2:#0:#neg:#pos:#s → :::nil:tuple#2:#0:#neg:#pos:#s
split :: :::nil:tuple#2:#0:#neg:#pos:#s → :::nil:tuple#2:#0:#neg:#pos:#s
split#1 :: :::nil:tuple#2:#0:#neg:#pos:#s → :::nil:tuple#2:#0:#neg:#pos:#s
splitAndSort :: :::nil:tuple#2:#0:#neg:#pos:#s → :::nil:tuple#2:#0:#neg:#pos:#s
splitqs#1 :: :::nil:tuple#2:#0:#neg:#pos:#s → :::nil:tuple#2:#0:#neg:#pos:#s → :::nil:tuple#2:#0:#neg:#pos:#s
splitqs#2 :: :::nil:tuple#2:#0:#neg:#pos:#s → :::nil:tuple#2:#0:#neg:#pos:#s → :::nil:tuple#2:#0:#neg:#pos:#s → :::nil:tuple#2:#0:#neg:#pos:#s
splitqs#3 :: #false:#true → :::nil:tuple#2:#0:#neg:#pos:#s → :::nil:tuple#2:#0:#neg:#pos:#s → :::nil:tuple#2:#0:#neg:#pos:#s → :::nil:tuple#2:#0:#neg:#pos:#s
#and :: #false:#true → #false:#true → #false:#true
#EQ :: #EQ:#GT:#LT
#GT :: #EQ:#GT:#LT
#LT :: #EQ:#GT:#LT
#0 :: :::nil:tuple#2:#0:#neg:#pos:#s
#neg :: :::nil:tuple#2:#0:#neg:#pos:#s → :::nil:tuple#2:#0:#neg:#pos:#s
#pos :: :::nil:tuple#2:#0:#neg:#pos:#s → :::nil:tuple#2:#0:#neg:#pos:#s
#s :: :::nil:tuple#2:#0:#neg:#pos:#s → :::nil:tuple#2:#0:#neg:#pos:#s
hole_#false:#true1_5 :: #false:#true
hole_:::nil:tuple#2:#0:#neg:#pos:#s2_5 :: :::nil:tuple#2:#0:#neg:#pos:#s
hole_#EQ:#GT:#LT3_5 :: #EQ:#GT:#LT
gen_:::nil:tuple#2:#0:#neg:#pos:#s4_5 :: Nat → :::nil:tuple#2:#0:#neg:#pos:#s
Generator Equations:
gen_:::nil:tuple#2:#0:#neg:#pos:#s4_5(0) ⇔ nil
gen_:::nil:tuple#2:#0:#neg:#pos:#s4_5(+(x, 1)) ⇔ ::(nil, gen_:::nil:tuple#2:#0:#neg:#pos:#s4_5(x))
The following defined symbols remain to be analysed:
#eq, #compare, append, append#1, insert, quicksort, quicksort#1, splitqs, sortAll, sortAll#1, split, split#1, splitqs#1
They will be analysed ascendingly in the following order:
append = append#1
append < quicksort#1
insert < split#1
quicksort = quicksort#1
quicksort < sortAll#1
splitqs < quicksort#1
splitqs = splitqs#1
sortAll = sortAll#1
split = split#1